Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
From LF Require Export IndProp.
From LF Require Export Rel.
From Coq Require Import Lia.

Theorem double_negation:
  (forall P, P \/ ~P) -> (forall P, ~~P <-> P).
Proof.
  intros.
  assert (P\/~P) as H1. { apply H. }
  split.
  - intros. destruct H1.
    + apply H1.
    + apply H0 in H1. inversion H1.
  - auto.
Qed.

Inductive last (n:nat):list nat->Prop :=
  | lbase: last n [n]
  | lstep: forall m l, last n l -> last n (m::l).

Example tst2: last 5 [1;2;3;4;5].
Proof. apply lstep. apply lstep. apply lstep. apply lstep. apply lbase. Qed.

Example tst3: forall n, ~(last n []).
Proof. intros n H. inversion H. Qed.

Inductive gt : nat->nat->Prop :=
  | gt_n: forall n, gt (S n) n
  | gt_S: forall m n, gt m n -> gt (S m) n.

Example test5: gt 3 1.
Proof. apply gt_S. apply gt_n. Qed.

Example gt_transitive : forall m n p,
  gt m n -> gt n p -> gt m p.
Proof.
  intros. induction H.
  - apply gt_S. apply H0.
  - apply gt_S. apply IHgt. apply H0.
Qed.
